T:Type, B:(T(Top + Top)), L:(T List).
concat(map(x.case B(x) of inl(a) => [a] | inr(a) => [];L))
~
mapfilter(x.outl(B(x));x.isl(B(x));L) 

latex

Definitions	t  T, x:A. B(x), Top, mapfilter(f;P;L), False, A, True, P  Q, b, b, , , isl(x), P & Q, P  Q, Unit, x(s), concat(ll)
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, isl wf, bool wf, bnot wf, assert wf, true wf, not wf, false wf, top wf